1. Field of the Disclosure
The present disclosure relates to symbolic execution for software testing and, specifically, to parameterized states in symbolic execution.
2. Description of the Related Art
With the ubiquitous presence of software programs permeating many aspects of daily life, software testing by validating and verifying software code to provide robust and reliable executable programs has become an important part of the software development process. Traditionally, software quality has been assured through manual software testing, which may be tedious, difficult, and may often give poor coverage of the software code. More recently, automated techniques for formal software testing have been developed. One such technique is symbolic execution.
Symbolic execution is a non-explicit state model-checking technique that treats input to a software program as symbol variables. Symbolic execution includes creation of complex equations by executing finite paths in the software program with symbolic variables and then solving the complex equations with a solver, typically known as a decision procedure, to obtain error scenarios, if any exist. In contrast to explicit state model checking, symbolic execution may be able to work out possible input values and possible use cases of the possible input values in a software program under analysis. Symbolic execution may be used to automatically generate test inputs with high structural coverage for the software under test. However, during symbolic execution, a very large number of execution paths and/or states may be generated that may limit the applicability of symbolic execution due to high consumption of computational resources.